Principles of Spin is an introductory book, the only requirement is a background in programming. Spin models are written in the Promela language which is easily learned by students and programmers. Spin is easy to install and use. The Spin model checker is not only a widely used professional tool but it is also a superb tool for teaching important concepts of computer science such as verification, concurrency and nondeterminism. The book introduces Spin-based software that the author has developed for teaching: jSpin - an integrated development environment for Spin. SpinSpider - uses output from Spin to automatically construct state diagrams of concurrent programs. VN is a tool for visualizing nondeterminism. Complete programs will demonstrate each construct and concept and these programs will be available on a companion website.

This open access book bridges the gap between playing with robots in school and studying robotics at the upper undergraduate and graduate levels to prepare for careers in industry and research. Robotic algorithms are presented formally, but using only mathematics known by high-school and first-year college students, such as calculus, matrices and probability. Concepts and algorithms are explained through detailed diagrams and calculations. Elements of Robotics presents an overview of different types of robots and the components used to build robots, but focuses on robotic algorithms: simple algorithms like odometry and feedback control, as well as algorithms for advanced topics like localization, mapping, image processing, machine learning and swarm robotics. These algorithms are demonstrated in simplified contexts that enable detailed computations to be performed and feasible activities to be posed. Students who study these simplified demonstrations will be well prepared for advanced study of robotics. The algorithms are presented at a relatively abstract level, not tied to any specific robot. Instead a generic robot is defined that uses elements common to most educational robots: differential drive with two motors, proximity sensors and some method of displaying output to the user. The theory is supplemented with over 100 activities, most of which can be successfully implemented using inexpensive educational robots. Activities that require more computation can be programmed on a computer. Archives are available with suggested implementations for the Thymio robot and standalone programs in Python.

This is open access book provides plenty of pleasant mathematical surprises. There are many fascinating results that do not appear in textbooks although they are accessible with a good knowledge of secondary-school mathematics. This book presents a selection of these topics including the mathematical formalization of origami, construction with straightedge and compass (and other instruments), the five- and six-color theorems, a taste of Ramsey theory and little-known theorems proved by induction. Among the most surprising theorems are the Mohr-Mascheroni theorem that a compass alone can perform all the classical constructions with straightedge and compass, and Steiner's theorem that a straightedge alone is sufficient provided that a single circle is given. The highlight of the book is a detailed presentation of Gauss's purely algebraic proof that a regular heptadecagon (a regular polygon with seventeen sides) can be constructed with straightedge and compass. Although the mathematics used in the book is elementary (Euclidean and analytic geometry, algebra, trigonometry), students in secondary schools and colleges, teachers, and other interested readers will relish the opportunity to confront the challenge of understanding these surprising theorems. Supplementary material to the book can be found at https://github.com/motib/suprises.

Mathematical Logic for Computer Science is a mathematics textbook with theorems and proofs, but the choice of topics has been guided by the needs of students of computer science. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and easy to understand. The uniform use of tableaux-based techniques facilitates learning advanced logical systems based on what the student has learned from elementary systems. The logical systems presented are: propositional logic, first-order logic, resolution and its application to logic programming, Hoare logic for the verification of sequential programs, and linear temporal logic for the verification of concurrent programs. The third edition has been entirely rewritten and includes new chapters on central topics of modern computer science: SAT solvers and model checking.